plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
TIMES(X, s(Y)) → TIMES(Y, X)
TIMES(X, s(Y)) → PLUS(X, times(Y, X))
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TIMES(X, s(Y)) → TIMES(Y, X)
TIMES(X, s(Y)) → PLUS(X, times(Y, X))
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(plus(X, Y), Z) → PLUS(Y, Z)
Used ordering: Polynomial interpretation [25,35]:
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
The value of delta used in the strict ordering is 16.
POL(PLUS(x1, x2)) = (4)x_1 + (4)x_2
POL(plus(x1, x2)) = 4 + x_1 + x_2
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(plus(X, Y), Z) → PLUS(X, plus(Y, Z))
The value of delta used in the strict ordering is 1/8.
POL(PLUS(x1, x2)) = x_1 + (1/2)x_2
POL(plus(x1, x2)) = 1/4 + x_1 + (1/2)x_2
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
TIMES(X, s(Y)) → TIMES(Y, X)
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(X, s(Y)) → TIMES(Y, X)
The value of delta used in the strict ordering is 1/2.
POL(TIMES(x1, x2)) = (4)x_1 + (2)x_2
POL(s(x1)) = 1/4 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
plus(plus(X, Y), Z) → plus(X, plus(Y, Z))
times(X, s(Y)) → plus(X, times(Y, X))